;;;============================================================
;;;
;;; Subject: logbitp
;;;         
;;;
;;;------------------------------------------------------------
;;;
;;;
;;;============================================================

#| Certification code:

(certify-book "logbitp" 0 nil)

|#

(in-package "ACL2")

(include-book "arithmetic-4/top" :dir :system)

(include-book "my-logbitp")

(include-book "dg-natural")

(set-verify-guards-eagerness 0)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;  1dlop-dgop-do = 1dlop-dgop-binary-do
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun 1dlop-dgop-do (d dgop)
  (or (logbitp d dgop)
      (and (> d 0)
	   (logbitp (- d 1) dgop))))

(defthm my-logbitp-logbitp-case-0
  (implies (natp dgop)
	   (equal (logbitp 0 dgop)
		  (my-logbitp 0 (dgn->dgb dgop))))
  :hints (("Goal" :in-theory (enable logbitp oddp ash evenp))))


(defun my-logbitp-logbitp-schema (d dgop)
  (if (or (not (natp d)) (not (> d 0)) (not (natp dgop)))
      nil
    (if (zp dgop)
	t
      (my-logbitp-logbitp-schema (- d 1) (ash dgop -1)))))

(defthm my-logbitp-logbitp
  (implies (and (natp d)
		(natp dgop))
	   (equal (logbitp d dgop)
		  (my-logbitp d (dgn->dgb dgop))))
:hints (("Goal"	 :induct (my-logbitp-logbitp-schema d dgop))))


(defthm my-logbitp-logbitp-b
  (implies (and (natp d)
		(dgb-p dgop))
	   (equal (my-logbitp d dgop)
		  (logbitp d (dgb->dgn dgop))
		  ))
:hints (("Goal" :do-not-induct t
	 :use
	 ((:instance my-logbitp-logbitp (dgop (dgb->dgn dgop)))))))



(defthm my-logbitp-logbitp-plusp
  (implies (and (natp d)
		(> d 0)
		(natp dgop))
	   (equal (logbitp (- d 1) dgop)
		  (my-logbitp (- d 1) (dgn->dgb dgop))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance my-logbitp-logbitp (d (- d 1)))))))

(defthm my-logbitp-logbitp-plusp-b
  (implies (and (natp d)
		(> d 0)
		(natp dgop))
	   (equal (logbitp (- d 1) (dgb->dgn dgop) )
		  (my-logbitp (- d 1) dgop)))
:hints (("Goal" :do-not-induct t
	 :in-theory (disable my-logbitp-logbitp-b
			     my-logbitp-logbitp-plusp)
	 :use ((:instance my-logbitp-logbitp-plusp 
			  (dgop (dgb->dgn dgop)))))))

(in-theory (disable my-logbitp-logbitp-plusp
		    my-logbitp-logbitp-plusp-b
		    my-logbitp-logbitp-b
		    my-logbitp-logbitp))

(defthm cadr-dgop=0-car-dgop=1=>my-logbitp-0
  (implies (and (= (cadr dgop) 0)
		(= (car dgop) 1)
		(dgb-p dgop))
	   (my-logbitp 0 dgop)))

(defthm cadr-dgop=0-car-dgop=1=>logbitp-0
  (implies (and (= (cadr dgop) 0)
		(= (car dgop) 1)
		(dgb-p dgop))
	   (logbitp 0 (dgb->dgn dgop)))
:hints (("Goal" :do-not-induct t
	 :use ((:instance cadr-dgop=0-car-dgop=1=>my-logbitp-0)
	       (:instance my-logbitp-logbitp-b
			  (d 0))))))


(defthm cadr-dgop=0-car-dgop=1=>not-my-logbitp-1
  (implies (and (= (cadr dgop) 0)
		(= (car dgop) 1)
		(dgb-p dgop))
	   (not (my-logbitp 1 dgop))))

(defthm cadr-dgop=0-car-dgop=1=>not-logbitp-1
  (implies (and (= (cadr dgop) 0)
		(= (car dgop) 1)
		(dgb-p dgop))
	   (not (logbitp 1 (dgb->dgn dgop))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance  cadr-dgop=0-car-dgop=1=>not-my-logbitp-1)
	       (:instance my-logbitp-logbitp-b
			  (d 1))))))

(defthm cadr-dgop=1=>my-logbitp-1
  (implies (and (= (cadr dgop) 1)
		(dgb-p dgop))
	   (my-logbitp 1 dgop)))

(defthm cadr-dgop=1=>logbitp-1
  (implies (and (= (cadr dgop) 1)
		(dgb-p dgop))
	   (logbitp 1 (dgb->dgn dgop)))
:hints (("Goal" :do-not-induct t
	 :use ((:instance cadr-dgop=1=>my-logbitp-1)
	       (:instance my-logbitp-logbitp-b
			  (d 1))))))




(defthm 1dlop-dgop-do=1dlop-dgop-binary-do
  (implies (and (natp d)
		(natp dgop))
	   (equal (1dlop-dgop-do d dgop)
		  (1dlop-dgop-binary-do d (dgn->dgb dgop))))
:hints (("Goal" :do-not-induct t
	 :use ((:instance my-logbitp-logbitp)
	       (:instance my-logbitp-logbitp-plusp)))))
